\begin{tabbing}
$\forall$${\it es}$:ES, $R$:\{$R$:E$\rightarrow$E$\rightarrow\mathbb{P}\mid$ $\forall$$e$, ${\it e'}$:E. $R$($e$,${\it e'}$) $\Rightarrow$ (${\it e'}$ $<$ $e$)\} .
\\[0ex]($\forall$$e$, ${\it e'}$:E. Dec($R$($e$,${\it e'}$)))
\\[0ex]$\Rightarrow$ ($\exists$\=$p$:E$\rightarrow$(E + Top)\+
\\[0ex](causal{-}predecessor(${\it es}$;$p$)
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex](($\uparrow$can{-}apply($p$;$e$)) $\Leftarrow\!\Rightarrow$ ($\exists$${\it e'}$:E. $R$($e$,${\it e'}$)))
\\[0ex]\& (($\uparrow$can{-}apply($p$;$e$)) $\Rightarrow$ $R$($e$,do{-}apply($p$;$e$))))))
\-\-
\end{tabbing}